es:ES, i, a, done:Id.
@i done initially ff:
 @i only [locl(a)] affect done:
 @i events of kind locl(a) change done to s,v. tt State(done : ) (val:Unit)
 @i Precondition for a(Outcome(*1*)) 
 @i s.(s(done)) discrete state(done : )
 (e@i. e'@i. (kind(e) = locl(a)  Knd)  (kind(e') = locl(a)  Knd)  (e = e'  E)
 & e@i.kind(e) = locl(a)  Knd) 

latex

Definitions

DeclaredType(ds;x), T, x. t(x), t.1, x:A. B(x), initial state @i, True, if b then t else f fi , P  Q, P  Q, A, {T}, SQType(T), (e <loc e'), e loc e' , P  Q, b, , t  T, Top, A c B, @i(x:T), e@i.P(e), Knd, e@i. P(e), P & Q, b, tt, @i events of kind k change x to f State(ds) (val:T), ff, P  Q, x:A. B(x), State(ds), x(s), state after e, e'e.P(e'), Dec(P), False, (state when e), @i Precondition for a(Outcome(p)) P discrete state(ds), Unit, @i only L affect x:T, , @i x initially v:T,

Lemmas

event system wf, bfalse wf, init-p wf, Knd wf, locl wf, es-frame wf, decl-state wf, btrue wf, unit wf, fpf-single wf3, effect-p wf, subtype rel self, eqof eq btrue, fpf-cap-single, Id wf, fpf-single wf, discrete-pre-p wf, or functionality wrt iff, es-first-init, es-when-first-discrete, squash wf, es-lc-no-change2, es-init-le, es-le-loc, Id sq, es-loc-init, pi1 wf, not-assert, true wf, false wf, es-initially wf, es-dds-single, es-dds wf, es-E wf, bnot wf, implies functionality wrt iff, assert of bnot, eqff to assert, iff transitivity, not wf, eqtt to assert, IdLnk wf, member singleton, l member wf, not functionality wrt iff, decidable equal Kind, bool sq, es-lc-cases2, es-locl wf, bool wf, es-lc-no-change, es-lc-le, es-causl wf, es-le wf, same-loc-total, es-when wf, es-after wf, es-lc wf, es-kind wf, es-dtype wf, es-vartype wf, es-loc wf, es-isconst wf, assert wf, bool-deq wf, es-loc-lc, id-deq wf, fpf-cap-single1